r, s:. (qpositive(r))  (qpositive(s))  (qpositive(r * s)) 

latex

Definitions	P  Q, i > j, P  Q, , P & Q, P  Q, ff, tt, 1/r, if b then t else f fi , t  T, (r/s), r * s, qpositive(r), P  Q, x:A. B(x), False, A, a  b  T , {T}, A c B, , x:A. B(x)
Lemmas	neg mul arg bounds, pos mul arg bounds, gt wf, rationals wf, qmul wf, qpositive wf, assert of lt int, and functionality wrt iff, assert of band, or functionality wrt iff, assert of bor, iff transitivity, lt int wf, band wf, bor wf, assert wf, implies functionality wrt iff, int nzero properties, q-elim